COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.s(intro, Introduction)
C00004 ENDMK
C⊗;
.s(intro, Introduction)

	This book is for readers who want to acquire both the
technique of programming in LISP and a mathematical understanding
of recursive programming.  The mathematical understanding offered
is at a more concrete level that provided by courses in recursive
function theory.  They are interested in what can be computed in
general and we develop techniques for proving particular properties
of particular programs, especially that they meet specifications
expressed as sentences in first order theorie.

	The reader of this book can learn two techniques.  The first
is programming in the LISP programming language.  LISP offers a
different way of looking at programming problems than Algol or
Fortran, and it has been the chosen language for most work in
artificial intelligence for twenty years.

	The second technique is that of proving that programs
meet their specifications together with the auxiliary technique
of expressing specifications as sentences in first order logic.

	This is probably the first textbook of programming that
emphasizes techniques for proving programs correct.